#pragma once

#include <stdio.h>
#include <stdlib.h>
#include <iostream>
#include "string.h"

using namespace std;
typedef int NodeId;


typedef enum {
	PDTNode_Em,
	PDTCodeGraph_Em,
	PDTExp_Em,
	PDTUnresolvedExp_Em,
	PDTExpNum_Em,
	PDTExpBool_Em,
	PDTUnaryNumExp_Em,
	PDTVar_Em,
	PDTConst_Em,
	PDTExpNumBin_Em,
	PDTExpNumUn_Em,
	PDTExpNumSing_Em,
	PDTNumVar_Em,
	PDTNumConst_Em,
	PDTNumConstInt_Em,
	PDTNumConstDbl_Em,
	PDTExpBoolBinBool_Em,
	PDTExpBoolBinNum_Em,
	PDTExpBoolBinBoolDerived_Em,
	PDTExpBoolBinNumDerived_Em,
	PDTExpBoolUn_Em,
	PDTExpBoolSing_Em,
	PDTBoolVar_Em,
	PDTBoolConst_Em,
	PDTLessThan_Em,
	PDTGreaterThan_Em,
	PDTLessThanEqual_Em,
	PDTGreaterThanEqual_Em,
	PDTEqualNum_Em,
	PDTImplies_Em,
	PDTXor_Em,
	PDTEqualBool_Em,
	PDTNotEqualNum_Em,
	PDTNotEqualBool_Em,
	PDTAdd_Em,
	PDTSubt_Em,
	PDTMult_Em,
	PDTDiv_Em,
	PDTMod_Em,
	PDTNeg_Em,
	PDTNot_Em,

	PDTStatement_Em,
	PDTIfElse_Em,
	PDTAssign_Em,
	PDTWhile_Em,
	PDTListOfStatements_Em,
	PDTAssert_Em,
	PDTCondition_Em,
	PDTPreCondition_Em,
	PDTPostCondition_Em,
	PDTInvariant_Em,
	PDTBehavior_Em,
	PDTProp_Em,
	PDTGoodAssignment_Em,
	PDTBadAssignment_Em,
    PDTSpecTriple_Em,

	PDTAnd_Em,
	PDTOr_Em,
	PDTFunctionDec_Em,
    PDTFunctionCall_Em,

	PDTSet_Em, // types
    PDTIntRange_Em,
	PDTSequence_Em,
	PDTArray_Em = PDTSequence_Em,
	PDTSequenceConst_Em,
	PDTPair_Em,
	PDTRelation_Em,

	PDTSetVar_Em,
    PDTSequenceVar_Em,

	PDTForall_Em,// Quantifiers
	PDTExist_Em,

	PDTUnion_Em,// Set expressions
	PDTIntersect_Em,
	PDTComplement_Em,

	PDTMember_Em, // Boolean set expressions
	PDTSubsetEq_Em,
	PDTCardinality_Em,// Cardinality
	PDTProduct_Em,// Relational or Cartesian product

	PDTSequenceAccessNum_Em, // Array access
	PDTSequenceAccessBool_Em,
    PDTMapConst_Em,

	NodeType_LastOne
} NodeTypeEnum;

typedef enum {
	UnaryMinus, // -
	UnaryPlus   // +
} UnaryOpEnum;

extern const char * PDTNodeTypeStringMap[NodeType_LastOne];
